Runtime Complexity (innermost) proof of /tmp/tmpHhxSKU/intersect.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

↳2 CdtProblem

↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳4 CdtProblem

↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳6 CdtProblem

↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳8 CdtProblem

↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳10 CdtProblem

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳12 CdtProblem

↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳14 CdtProblem

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳16 CdtProblem

↳17 CdtKnowledgeProof (⇔)

↳18 CdtProblem

↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳20 CdtProblem

↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳22 CdtProblem

↳23 SIsEmptyProof (⇔)

↳24 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

K tuples:none
Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

IFMEM(false, z0, z1) → c12(MEM(z0, z1))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = 0
POL(EQ(x₁, x₂)) = 0
POL(IFINTER(x₁, x₂, x₃, x₄)) = x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = [1] + x₃
POL(INTER(x₁, x₂)) = x₁·x₂
POL(MEM(x₁, x₂)) = x₂
POL(app(x₁, x₂)) = [2]x₁ + x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = [2] + x₁ + x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = 0
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = 0
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = 0
POL(EQ(x₁, x₂)) = 0
POL(IFINTER(x₁, x₂, x₃, x₄)) = x₃ + x₄ + x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = 0
POL(INTER(x₁, x₂)) = x₁ + x₂ + x₁·x₂
POL(MEM(x₁, x₂)) = 0
POL(app(x₁, x₂)) = [2] + [2]x₁ + x₂ + [2]x₁·x₂ + [2]x₁²
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = 0
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = 0
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = 0
POL(EQ(x₁, x₂)) = 0
POL(IFINTER(x₁, x₂, x₃, x₄)) = x₃·x₄ + x₂·x₄
POL(IFMEM(x₁, x₂, x₃)) = x₃
POL(INTER(x₁, x₂)) = x₁·x₂
POL(MEM(x₁, x₂)) = x₂
POL(app(x₁, x₂)) = [2]x₁ + [2]x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = [1] + x₁ + x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = 0
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = 0
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = 0
POL(EQ(x₁, x₂)) = x₁·x₂
POL(IFINTER(x₁, x₂, x₃, x₄)) = [2]x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = x₂·x₃
POL(INTER(x₁, x₂)) = [2]x₁·x₂
POL(MEM(x₁, x₂)) = x₁·x₂
POL(app(x₁, x₂)) = [2]x₁ + x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = 0
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = 0
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = [1] + x₁
POL(true) = 0

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = 0
POL(EQ(x₁, x₂)) = 0
POL(IFINTER(x₁, x₂, x₃, x₄)) = x₃ + x₄ + x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = 0
POL(INTER(x₁, x₂)) = x₁ + x₂ + x₁·x₂
POL(MEM(x₁, x₂)) = 0
POL(app(x₁, x₂)) = [1] + x₁ + x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = [1] + x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = 0
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = 0
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = 0
POL(EQ(x₁, x₂)) = 0
POL(IFINTER(x₁, x₂, x₃, x₄)) = [2] + x₃ + [2]x₄ + x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = 0
POL(INTER(x₁, x₂)) = x₁ + x₂ + x₁·x₂
POL(MEM(x₁, x₂)) = 0
POL(app(x₁, x₂)) = [2] + [2]x₁ + [2]x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = [2] + x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = 0
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = 0
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(APP(x₁, x₂)) = 0
POL(EQ(x₁, x₂)) = x₁ + [3]x₂
POL(IFINTER(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₄ + [3]x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = x₁ + [3]x₃ + [3]x₂·x₃
POL(INTER(x₁, x₂)) = [3]x₁·x₂
POL(MEM(x₁, x₂)) = [3]x₂ + [3]x₁·x₂
POL(app(x₁, x₂)) = x₁ + x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = [3] + x₁ + x₂
POL(eq(x₁, x₂)) = [3] + x₁
POL(false) = [2]
POL(ifinter(x₁, x₂, x₃, x₄)) = 0
POL(ifmem(x₁, x₂, x₃)) = [2] + [2]x₃
POL(inter(x₁, x₂)) = 0
POL(mem(x₁, x₂)) = [2]x₂
POL(nil) = [2]
POL(s(x₁)) = x₁
POL(true) = [2]

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(17) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = [1] + [2]x₁
POL(EQ(x₁, x₂)) = 0
POL(IFINTER(x₁, x₂, x₃, x₄)) = x₃ + x₄ + [3]x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = 0
POL(INTER(x₁, x₂)) = x₁ + x₂ + [3]x₁·x₂
POL(MEM(x₁, x₂)) = 0
POL(app(x₁, x₂)) = [1] + [3]x₁ + x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄ + [3]x₃·x₄
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = x₁ + x₂ + [3]x₁·x₂
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:

APP(cons(z0, z1), z2) → c7(APP(z1, z2))

K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APP(cons(z0, z1), z2) → c7(APP(z1, z2))

We considered the (Usable) Rules:

mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))

And the Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(APP(x₁, x₂)) = [3] + [2]x₁
POL(EQ(x₁, x₂)) = 0
POL(IFINTER(x₁, x₂, x₃, x₄)) = [3]x₃ + [3]x₄ + [3]x₃·x₄
POL(IFMEM(x₁, x₂, x₃)) = 0
POL(INTER(x₁, x₂)) = [3]x₁ + [3]x₂ + [3]x₁·x₂
POL(MEM(x₁, x₂)) = 0
POL(app(x₁, x₂)) = [3] + [3]x₁ + x₂
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c15(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c16(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = [1] + x₂
POL(eq(x₁, x₂)) = 0
POL(false) = 0
POL(ifinter(x₁, x₂, x₃, x₄)) = [3] + [3]x₃ + [3]x₄ + [3]x₃·x₄
POL(ifmem(x₁, x₂, x₃)) = 0
POL(inter(x₁, x₂)) = [3]x₁ + [3]x₂ + [3]x₁·x₂
POL(mem(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)

Tuples:

EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))

S tuples:none
K tuples:

IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))

Defined Rule Symbols:

if, eq, app, mem, ifmem, inter, ifinter

Defined Pair Symbols:

EQ, APP, MEM, IFMEM, INTER, IFINTER

Compound Symbols:

c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20

(23) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(4) Obligation:

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(6) Obligation:

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(8) Obligation:

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(10) Obligation:

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(12) Obligation:

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(14) Obligation:

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(16) Obligation:

(17) CdtKnowledgeProof (EQUIVALENT transformation)

(18) Obligation:

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(20) Obligation:

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(22) Obligation:

(23) SIsEmptyProof (EQUIVALENT transformation)

(24) BOUNDS(O(1), O(1))